feat(Logics/Temporal/Syntax): temporal formula type and syntax utilities#642
Closed
benbrastmckie wants to merge 5 commits into
Closed
feat(Logics/Temporal/Syntax): temporal formula type and syntax utilities#642benbrastmckie wants to merge 5 commits into
benbrastmckie wants to merge 5 commits into
Conversation
Introduces bot/imp as primitive Proposition constructors (replacing and/or/impl), adds Connectives.lean typeclass hierarchy for derived connectives, simplifies NaturalDeduction/Basic.lean from 10 rules to 5, and adds ChagrovZakharyaschev1997 reference. Session: sess_1781224549_831844
…ilities Adds Formula.lean (582 lines), Context.lean (131 lines), BigConj.lean (52 lines), and Subformulas.lean (218 lines) to Cslib/Logics/Temporal/Syntax/.
… citations - Add 4 Cslib.Logics.Temporal.Syntax.* entries to Cslib.lean barrel - Add Kamp1968 and GabbayPnueliShelahStavi1980 entries to references.bib - Update Formula.lean ## References to use [BibKey] bracket format
benbrastmckie
requested review from
arademaker,
chenson2018 and
fmontesi
as code owners
benbrastmckie
added a commit
to benbrastmckie/cslib
that referenced
this pull request
Jun 13, 2026
… syntax Created pr3/temporal-syntax branch from refactor/proposition-lukasiewicz, cherry-picked all 4 temporal syntax files, added BibTeX entries and BibKey citations, added 4 barrel imports to Cslib.lean, passed full CI pipeline, and submitted PR leanprover#642 to leanprover/cslib. PR URL: leanprover#642 Session: sess_1781307197_e61477
benbrastmckie
added a commit
to benbrastmckie/cslib
that referenced
this pull request
Jun 14, 2026
… syntax Created pr3/temporal-syntax branch from refactor/proposition-lukasiewicz, cherry-picked all 4 temporal syntax files, added BibTeX entries and BibKey citations, added 4 barrel imports to Cslib.lean, passed full CI pipeline, and submitted PR leanprover#642 to leanprover/cslib. PR URL: leanprover#642 Session: sess_1781307197_e61477
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Cslib.Logics.Temporal.Syntax.Formula(582 lines): core temporal formula inductive typeFormula Atomwith primitives{atom, bot, imp, untl, snce}, BEq/Countable/Denumerableinstances, complexity/depth measures, derived operators (F, G, P, H, W, B, etc.), swap duality
theorem, and atom enumeration
Cslib.Logics.Temporal.Syntax.Context(131 lines): formula list type for proof contextswith
And/Or/Implieslifting, context difference, and formula membership instancesCslib.Logics.Temporal.Syntax.BigConj(52 lines): big conjunction fold over formula listswith simplification lemmas
Cslib.Logics.Temporal.Syntax.Subformulas(218 lines): subformula closure withdecidability, cardinality bounds, and atom content
Cslib.leanbarrel with 4 newLogics.Temporal.Syntax.*import entriesKamp1968andGabbayPnueliShelahStavi1980entries toreferences.bibDependencies
This PR depends on PR #635 (
feat(Foundations/Logic): Connectives typeclass)because
Formula.leanimportsCslib.Foundations.Logic.Connectivesfor theTemporalConnectivestypeclass. This PR is stacked on top of PR #635's branch
(
benbrastmckie:refactor/proposition-lukasiewicz) and will not be mergeable until PR #635 merges.The temporal syntax files themselves are pure syntax — they contain no proofs beyond
decideautomation, BEq instances, and basic structural lemmas.
Scope
This PR covers Sub-PR 3.1 (temporal formula type) and Sub-PR 3.2 (syntax utilities). The
utility files (Context, BigConj, Subformulas) have exactly one dependency —
Formula.lean—and are pure syntax with no proofs, keeping the combined diff reviewable at ~983 lines.
Subsequent temporal PRs (axioms, derivation, proof system instances, semantics) will follow
in separate stacked PRs.
Files Changed
Cslib/Logics/Temporal/Syntax/Formula.leanCslib/Logics/Temporal/Syntax/Context.leanCslib/Logics/Temporal/Syntax/BigConj.leanCslib/Logics/Temporal/Syntax/Subformulas.leanCslib.leanreferences.bib(The PR diff also includes changes from PR #635 since this branch stacks on top of it.)
CI Status
All CI checks pass on this branch (built on top of PR #635 base):
lake build --wfail --iofail— no errors or warnings in new fileslake exe checkInitImports— all files importCslib.Init(transitively viaConnectives)lake exe lint-style— passeslake exe mk_all --check --module— barrel completeness verifiedlake test— test suite passesAI Tools Used
cslib-implementation-agent, powered by Claude Sonnet 4.6): created the cleanpr3/temporal-syntaxbranch fromrefactor/proposition-lukasiewicz, added the barrel importsto
Cslib.lean, added the two BibTeX entries toreferences.bib, updated the## Referencessection in
Formula.leanto use[BibKey]bracket format per CSLib standards, fixed a100-character line-length linter violation in the citation, and ran the full CI verification
pipeline locally. The temporal syntax source files (
Formula.lean,Context.lean,BigConj.lean,Subformulas.lean) were authored by the human contributor (Benjamin Brast-McKie)prior to this PR submission task.